Termination Proof Script

• Consider the SCC {17,21,23-26}. The usable rules are {1,4,5,8-14}. By taking the AF π with π(activate) = π(ACTIVATE) = π(from) = π(n__from) = π(n__s) = π(s) = 1 and π(cons) = π(TAKE) = 2 together with the lexicographic path order with precedence 0 ≻ nil and n__take ≈ take, the rules in {1,5,8-14,17,21,23} are weakly decreasing and the rules in {4,24-26} are strictly decreasing. There is one new SCC.
  • Consider the SCC {21,23}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(n__from) = 1 together with the lexicographic path order with empty precedence, rule 21 is weakly decreasing and rule 23 is strictly decreasing. There is one new SCC.
    • Consider the SCC {21}. By taking the AF π with π(ACTIVATE) = 1 together with the lexicographic path order with empty precedence, rule 21 is strictly decreasing.


• Consider the SCC {18}. The usable rules are {1,4,5,8-14}. By taking the AF π with π(activate) = π(n__take) = π(SEL) = π(take) = 1, π(cons) = 2 and π(from) = π(n__from) = [ ] together with the lexicographic path order with precedence 0 ≻ nil, n__from ≈ from and n__s ≈ s, the rules in {1,8-14} are weakly decreasing and the rules in {4,5,18} are strictly decreasing.